COMMENT ⊗   VALID 00006 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\magnification\magstephalf
C00013 00003	\def\Lemma#1{\par\noindent{\bf Lemma #1}\quad}
C00015 00004	\prob {1}
C00020 00005	\prob{2.1}
C00026 00006	\prob{3}  The proof of the first result is quite long, if you are careful
C00039 ENDMK
C⊗;
\magnification\magstephalf
\input mathmo.fix[b2,jmc]
\def\prob#1{{\bf Problem #1}\par}
\catcode`|=13
\def|#1|{\hbox{\it#1\/}}
\parindent 0pt
\parskip 0pt
\def\pskip{\penalty-1000\vskip 6pt plus 2pt minus 1pt}
\def\ppskip{\penalty-2000\vskip 10pt plus 3pt minus 2pt}
\def\no(#1){\noindent\hbox to 6em{(#1)\hfill}}
\catcode`⊗=13
\def⊗{\hbox to 2em{}}
\def\IF{\mathop{\hbox{\bf if}}}
\def\THEN{\mathrel{\bf then}}
\def\ELSE{\mathrel{\bf else}}
\def\AND{\mathrel{\bf and}}
\def\OR{\mathrel{\bf or}}
\def\NOT{\mathop{\hbox{\bf not}}}
\def\N{\mathop{\hbox{\bf n}}}
\def\T{\hbox{\tt T}}
\def\NIL{\hbox{\tt NIL}}
\def\.{\mathrel{\raise .3ex\hbox{$\scriptscriptstyle{\bullet}$}}}
\def\A{\mathop{\hbox{\bf a}}}
\def\D{\mathop{\hbox{\bf d}}}
\def\EQ{\mathrel{\bf eq}}
\def\AT{\mathop{\hbox{\bf at}}}
\def\quote#1{\hbox{\sfcode`.=1000\tt#1}}
\def\list#1{\langle#1\rangle}
\def\xskip{\hskip7pt plus3pt minus4pt}

{\catcode`\↑↑M=13\global\let ↑↑M=\linebreak}	% This must be on one line!
\def\lines{\par\groupbegin
	\catcode`\ =12
	\sfcode`.=1000
	\parindent 0pt
	\leftskip 25pt
	\rightskip 0pt plus 1fil
	\interlinepenalty 50
	\baselineskip 12pt
	\parskip 12pt plus 6pt minus 6pt
	\catcode`\↑↑M=13
	\tt\eat}
\def\eat#1{}					% to eat the first <cr>
\def\endlines{\par\vskip\minusthe\baselineskip	% cancel the last empty line
	\vskip\the\parskip			% put in space
	\groupend\vskip\minusthe\parskip}	% cancel the next space to go in

\def\palign#1{\vcenter{\openup1\jot\mathsurround=0pt
  \ialign{\strut\hskip\parindent\hfil$\displaystyle{##}$&
  $\displaystyle{{}##}$\hfil&\quad##\hfil\crcr#1\crcr}}}

\line{CS 206 Autumn 1984\hfil Handout 16}
\centerline{\bf Homework 3 Solutions}

\ppskip
\def\Lemma#1{\par\noindent{\bf Lemma #1}\quad}
\def\Corollary#1{\par\noindent{\bf Corollary #1}\quad}
\def\Proposition#1{\par\noindent{\bf Proposition #1}\quad}
\def\Theorem:{\par\noindent{\bf Theorem:}\quad}
\def\Proof:{\par\noindent{\bf Proof:}\quad}
\def\samelength{\mathop{\it samelength}}
\def\reverse{\mathop{\it reverse}}
\def\length{\mathop{\it length}}
\def\istail{\mathop{\it istail}}
\def\com{commontail}
\def\upto{\mathop{\it upto}}


\ppskip
\prob {1}
Here is the most popular way to prove this result.
\pskip
\Lemma: $∀x u  v.  length[u*v] = length u + length v$.
\pskip
\Proof: We will prove the lemma by list induction on $u$:
so $\Phi(u) ≡ ∀v.  length[u*v] = length u + length v$.
First, $\Phi(\NIL)$ is $∀v. length [\NIL*v]=length \NIL + length v$.
But, from the definition of $length$, $length \NIL = 0$, and it is shown
on page 37 of chapter 3 that $\NIL * v = v$.  The result for $\Phi(\NIL)$
follows.
\pskip
Now, assume $\Phi(u)$ as an inductive hypothesis; then we have
$$\palign{
length[x\.u *v]&= 1 + length[\D[x\.u*v]] & (definition of $length$).\cr
	       &= 1 + length[u*v]\cr
	       &= 1 + length\,u + length\,v\cr
	       &= length \,x\.u + length \,v.\cr
}$$
This completes the lemma.
\pskip
\Theorem: $∀u. length u = length reverse u $.
\pskip
\Proof: By list induction on $u$, with $\Phi(u) ≡ length u = length reverse u$.
$\Phi(\NIL)$ is trivial (apply the definitions of $reverse$ and $length$).
Assuming $\Phi(u)$, $\Phi(x\.u)$ is
$$\palign{
length reverse [x\. u] &= length[ reverse u * <x>] & (definition of reverse)\cr
		       &= length reverse u + length <x> & (lemma)\cr
		       &= length reverse u + 1          & (definition of length)\cr
		       &= length u + 1			&(inductive hypothesis)\cr
		       &= length x\.u			&(definition of length)\cr
}$$
A number of people stated that if $u$ is a list, then $\A u$ is an atom. 
This is not true, $\A u$ can be any S-expression, but it is not
necessary to assume that result for the proof.
\ppskip
\prob{2.1}
\pskip
Let $\Phi(u)$ be $istail[\com[u,v],v]$.  Then $\Phi(\NIL)$ is
seen to be true by applying the function definitions.  Next assume $\Phi(u)$.
$$\palign{
\Phi(x\.u) &≡ istail[\com[x\.u,v],v]\cr
&=istail[\IF istail[x\.u,v]\THEN x\.u\ELSE\com[u,v],v]\cr
&=\IF\istail[x\.u,v]\THEN\istail[x\.u,v]\ELSE\istail[\com[u,v],v]\cr
}$$
which is valid, applying the inductive hypothesis.  Since no assumptions were
made about $v$, we can quantify over $v$, completing the inductive step.

\ppskip
\prob{2.2}. Let $\Phi(u)$ be $istail[\com[u,v],u]$.  Again $\Phi(\NIL)$
is easy to prove by applying the definitions, and assuming $\Phi(u)$ as an
inductive hypothesis, $\Phi(x\.u)$ is
$$\palign{
istail&[\com[x\.u,v],x\.u]\cr
&≡ istail[\IF istail[x\.u,v]\THEN x\.u\ELSE\com[u,v],x\.u]\cr
&≡\IF istail[x\.u,v]\THEN istail[x\.u,x\.u]\ELSE istail[\com[u,v],x\.u]\cr
}$$
If $ istail[x\.u,v]$ holds, then this becomes true since $ istail[x\.u,x\.u]$.
Otherwise, we get
$$\palign{
istail&[\com[u,v],x\.u]\cr
&≡\com[u,v]=x\.u\OR[\NOT\N[x\.u]\AND istail[\com[u,v],u]]\cr
}$$
which becomes true by using the inductive hypothesis.

\ppskip
\prob{2.3} 
First we require some preliminary results.
\pskip
\Lemma: $∀v. istail[\NIL, v]$.
\pskip
\Proof: by list induction on v, with $\Phi(v)$ being $istail[\NIL,v]$.
$\Phi(\NIL)$ follows immediately from the definition of $istail$.
Assuming $\Phi(v)$, we have 
$\Phi(y\.v) ≡ y\.v = \NIL ∨ [¬\N y\.v ∧ istail[\NIL,v]$
But no cons is equal to \NIL and $istail[\NIL,v]$ is the induction hypothesis,
so $\Phi(y\.v)$ holds, and we are done.
\pskip
\Lemma: $∀v. \com[\NIL, v] = \NIL$.
\Proof: Expand the definition of $\com$, and use the previous lemma.
\pskip
Now we come to the main result.
\pskip
Several people attempted to prove this by induction on $w$.  This
is reasonable as a first try, but it turns out that it doesn't work.  The 
following list induction on $u$ is correct.
\pskip
\Proof:
Let $\Phi(u)$ be $$istail[w,u] ∧ istail[w,v] ⊃ istail[w,\com[u,v]].$$
So$$\Phi(\NIL) ≡ istail[w,\NIL] ∧ istail[w,v] ⊃ istail[w,\NIL]$$
using the lemma.  But this is trivially true, since the consequent is
assumed in the antecedent.
\pskip
Now assume $\Phi(u)$, and that $istail[w,x\.u]$ and $istail[w,v]$.
\pskip
Since $istail[w,x\.u]$, we must have either that $w=x\.u$ or that
$istail[w,u]$, by expanding the definition of $istail$,
\pskip
If $istail[x\.u,v]$ then $\com[x\.u,v] = x\.u$ by definition of
$\com$ and so 
$$istail[w, \com[x\.u,v]] = istail[w,x\.u].$$  But we have already
assumed this statement, so the required result holds.
\ppskip
If $istail[w,u]$ then we have both $istail[w,u]$, and $istail[w,v]$
so we can use the inductive hypothesis to conclude $istail[w, \com[u,v]]$
Now consider
$$\palign{
istail&[w, \com[x\.u,v]]\cr
  &= istail[w, \IF istail[x\.u, v] \THEN	x\.u \ELSE \com[u,v]]\cr
  &= \IF istail[x\.u, v] \THEN istail[w, x\.u] \ELSE istail[w, \com[u,v]]\cr
}$$
We have assumed $istail[w, x\.u]$ and derived istail[w, \com[u,v]], so
the required result is proven.
\pskip
The most common mistake was to assume that $istail[w,\com[u,v]]$ was true,
without first showing the antecedents of $\Phi(u)$.
\ppskip
\prob{3}  The proof of the first result is quite long, if you are careful
to cover all the details.  The main difficulty is to prove that the
depth of the |car| and |cdr| of $balance[x]$ differ by at most 1.

\pskip
The following proof is due to Li-Mei Wu.

\pskip
\Lemma{1}
$$\eqalign{∀n u \hbox{such that} 0 ≤ n ≤ length[u]\hidewidth\cr
length[firstn[u,n]&=n\cr
length[restn[u,n]&=length[u]\minus n\cr
firstn[u,n]*restn[u,n]&= u\cr}$$

\pskip
\Proof: Is by induction on $n$.  (An induction on $u$ can also work,
but the induction on $n$ is more straightforward.)
\pskip
{\bf Base Case}: $n=0$
This case is shown by expanding the definitions of $firstn$, $restn$
and $length$.

{\bf Inductive Step}: Assume the lemma holds for $n\minus 1$, and that
$length[u]≥n$.  Since $n>0$ this implies that $u≠\NIL$, by a simple induction
using the definition of $length$.

$$\palign{
length[firstn[u,n]] &= length[\A u\.firstn[\D u, n\minus1]]&(definition of $firstn$)\cr
		    &= 1+length[firstn[\D u, n\minus1]]&(definition of $length$)\cr
		    &= n	&(by the inductive hypothesis)\cr
}$$

$$\palign{
length[restn[u,n]] &= length[restn[\D u, n\minus1]]&(definition of $firstn$)\cr
		    &= length[\D u] \minus( n \minus1)&(inductive hypothesis)\cr
		    &= length[u] \minus 1 \minus (n \minus 1)&(def. of $length$)\cr
		    &= length[u] \minus n\cr
}$$

$$\palign{
firstn[u,n]*restn[u,n]&=(\A u\.firstn[\D u,n\minus1])*restn[\D u,n\minus1]&(def. of $firstn$, $restn$)\cr
&=\A u\.(firstn[\D u,n\minus1])*restn[\D u,n\minus1]&(associativity)\cr
&=\A u\.\D u&(inductive hypothesis)\cr
}$$
\pskip
A corollary follows from this lemma immediately, using the definitions of
$fhalf$ and $shalf$:
\Corollary2
$$\eqalign{
∀u: length[fhalf u]&=\lfloor{length u\over2}\rfloor\cr
    length[shalf u]&=\lceil{length u\over2}\rceil\cr
    fhalf u * shalf u &= u\cr}$$

\ppskip
\def\F{{\cal F}}
\def\L{{\cal L}}
Let $\F$ be the class of non-null lists whose elements are all
atoms.  More formally $\F$ is defined by 
\hskip\parindent i)$\AT a ⊃ <a> ε \F$\par
\hskip\parindent ii)$\AT a ∧ u ε \F ⊃ a\.u ε \F$\par
\pskip
The next set of propositions prove some facts about $\F$.
\pskip
\Proposition3 If $xε\F$ then $xε\L$ (i.e. $x$ is a list).
\Proof: This is a slightly unusual proof, because we are not proving
any facts about programs.  In fact it could be transformed into a
regular proof by defining functions to recognize the two classes.
\pskip
The proof is by S-expression induction.

{\bf Base Case}: $x$ is an atom.  Then $x\notε\F$, because neither clause
of the definition of \F allows atoms, so the proposition holds trivially.

{\bf Inductive Step}: Suppose 
the proposition holds for $\A x$ 
and $\D x$, and $xε\F$.  Then either $x=<a>$ or $x=a\.y$ with $yε\F$,
and $a$ an atom.
In the first case we have $xε\L$ immediately.  In the second case,
$y=\D x$, so the inductive hypothesis holds for $y$, hence $yε\L$.  But
$x=a\.yε\L$, completing the induction.

\pskip
This result means that we are justified in using list induction to
prove results about \F, and that we can use functions defined on lists
on elements of \F.

\ppskip
\Proposition4. $u,vε\F ⊃ u*v ε\F$.
\Proof: by list induction on $u$.  Note that \NIL\ is not in \F, so
the base case of the induction is when $u=<a>$.

{\bf Base Case} $u=<a>$, so $u*v=<a>*v=a.vε\F$, by clause (ii) of the definition.

{\bf Inductive Step}.  Assume that $length u ≥ 2$ and 
the result holds for $\D u$.  Now
$u*v=\A u \. [\D u * v]$, but $uε\F$, so we must have $\AT \A u$ (since
both clauses of the definition imply this).  Further, since $length u ≥ 2$,
$u$ must be in \F because of clause (ii).  Hence, $\D u ε \F$.  Applying
the inductive hypothesis, $\D u * v ε \F$.  But then $\A u \. [\D u * v] ε \F$,
which is the required result.

\ppskip
\Proposition5. $∀x. fringe x ε \F$.
\Proof: by S-expression induction on $x$.
If $\AT x$ then $fringe x = <x>$, which is in \F\ by clause (i).
Otherwise, we assume the result holds for $\A x$ and $\D x$.  $fringe x =
[fringe \A x] * [fringe \D x]$.  But both of these are in \F, so the result
follows from proposition 1.

\ppskip
\Proposition6. $0<n<length u ∧ u ε \F ⊃ firstn[u,n] ε \F ∧ restn[u,n] ε \F$
\Proof: by induction on $n$.

{\bf Base Case} $n=1$.  Since $n<length x$ we must have $length x ≥ 2$.
Now $firstn[u,1]=<\A u>ε\F$, because $uε\F$, so $\AT\A u$.
$restn[u,1]=\D u$, which is in \F\ by clause (ii).

{\bf Inductive Step} $n ≥ 2$. $first[u,n] = \A u\.first[u, n\minus1]$.  This
is in \F\ by clause (ii) and the inductive hypothesis.\par
Now note that $2≤n<length x$, so $length rest[x,n\minus1] ≥ 2$, by lemma 1.
So if $rest[x,n\minus 1]ε\F$ it must be by clause (ii), and therefore 
$\D rest[x,n\minus 1]ε\F$, but this expression is equal to $rest[x,n]$,
completing the inductive step.

\ppskip
\Corollary7. $uε\F ∧length u ≥ 2 ⊃ fhalf u ε \F ∧ shalf u ε \F$.
\Proof: follows from proposition 6 and the definitions of $fhalf$ and $shalf$.

\ppskip
Finally we get to the important lemma which will enable us to prove the
result.
\pskip
\Lemma{8} If $uε\F$ then $depth bal u = \lceil\log↓2[length u]\rceil$
\Proof: Is by list induction on $u$.  The base case, $u=<a>$, is simply
a matter of expanding the definitions of $bal$ and $depth$.
\pskip
For the induction step, suppose $length u ≥ 2$, and
that the lemma holds for all $vε\F$ such that $length v < length u$.

We have 
$$\palign{
depth bal u &= depth[bal fhalf u \. bal shalf u]&(def of $bal$)\cr
&=1+\max[depth bal fhalf u, depth bal shalf u]&(def of $depth$)\cr
}$$
But from the corollary, and using the assumption that $length u ≥ 2$, we have 
$$\eqalign{
1 ≤ length fhalf u = \lfloor{length u \over 2}\rfloor < length u\cr
1 ≤ length shalf u = \lceil{length u \over 2}\rceil < length u\cr
}$$

Moreover, $fhalf u$ and $shalf u$ are in $\F$ from lemma x, so the 
inductive hypothesis can be used to show
$$\palign{
depth bal u &= 1 + \lceil\log↓2\lceil{length u\over 2}\rceil\rceil\cr
&=\lceil\log↓2[2\lceil{length u\over 2}\rceil\rceil&(by properties of ceil and log)\cr
}$$
Now, by considering the cases where $length u$ is even and odd separately, it
is simple to show the required result.
\ppskip
\Lemma{9} If $uε\F$ then $balanced bal u$.
\Proof: Is a list induction on $u$, with $\Phi(u)$ the statement of the lemma.

{\bf Base Case:} 
$u=<a>$.
Follows immediately from the definition of $balanced$ and $bal$.

{\bf Induction Step}: Assume $length u ≥ 2$ and assume the induction 
hypothesis for all $v$ with $length v < length u$.
$$\eqalign{
balanced bal u &= balanced[[bal fhalf u] \.[bal shalf u]]\cr
&=balanced bal fhalf u\cr
&\ ∧ balanced bal shalf u\cr
&\ ∧ \left\vert depth[bal fhalf u] \minus depth [bal shalf u]\right\vert ≤ 1\cr
}$$

\pskip
The first two conjuncts in this statement follow immediately from corollary 2,
and the inductive hypothesis.  The third conjunct follows from
lemma 8, and some arithmetic.  (Consider the two cases when $length u$ is 
odd and even separately.)
\ppskip
\Lemma{10} If $uε\F$ then $fringe bal u = u$.
\Proof: By list induction on $u$.  The base case is when $u=<a>$, and
is shown by expanding bal and fringe.
\pskip
For the inductive step suppose that $length u ≥ 2$ and that the inductive
hypothesis holds for all shorter $v$.  Then
$$\palign{
fringe bal u &= fringe [bal[fhalf u]\.bal[shalf u]]&(def of $bal$)\cr
&=fringe[bal[fhalf u]] * fringe[bal[shalf u]]&(def of $fringe$)\cr
&=fhalf u * shalf u&(ind. hypothesis)\cr
&=u&(corollary 2)\cr
}$$

\ppskip
The proofs of the two results follow immediately from lemmas 9 and 10, and
proposition 5.